package org.tau.workshop2011.semantics

import scala.collection.mutable.{Map => MutableMap, HashMap => MutableHashMap}
import scala.collection.mutable.{Set => MutableSet, HashSet => MutableHashSet}
import org.tau.workshop2011.parsing.AST._
import java.lang.AssertionError
import org.tau.workshop2011.expressions.Type

/**
 * Rules for READ-ONLY properties:
 * 1. A property is read-only if it's defined as a constant expression
 * 2. A property is read-only if it's definition is made out only of constants
 *    expressions and other read-only properties
 * 3. A property is read-only if it is defined by a conditional expression
 * 4. A property is read-only if it depends on a property defined by a
 *    conditional expression
 * 5. A property is read-only if it depends on 2 or more properties which aren't
 *    defined by an expression (and are defined only by an initial value - we
 *    call these free variables), because then we have the conflict of not
 *    knowing which property to update
 * 6. An integer property is read-only if it's defined by a non-linear expression
 *
 * Integer Expressions
 * ~~~~~~~~~~~~~~~~~~~
 * An integer expression is reversible (hence not read-only) if and only if ALL
 * of the following conditions hold:
 *
 * 1. It does not depend on a conditional expression, directly or indirectly
 * 2. After recursively expanding all it's dependencies, it depends on exactly
 *    one free variable
 * 3. After that expansion, the expression is linear with that variable
 *
 * Boolean Expressions
 * ~~~~~~~~~~~~~~~~~~~
 * A boolean expression is reversible (hence not read-only) if and only if ANY
 * of the following conditions hold:
 *
 * 1. It's defined simply as the value of a variable, where that variable is a
 *    free variable
 * 2. It's defined simply as the value of a variable, where that variable is
 *    defined with a reversible expression
 * 3. It's a comparison between a variable and a literal.
 *    In that case we only allow assignments of `true` into that expression
 *    (assignments of `false` will be ignored, and will log a warning)
 * 4. It's a conjunction of several expressions where all of them are either
 *    constant and evaluate to `true`, or simply reversible themselves.
 *    In that case we only allow assignments of `true` into that expression
 *    (assignments of `false` will be ignored, and will log a warning)
 * 5. It's a disjunction of several expressions where all of them are either
 *    constant and evaluate to `false`, or simply reversible themselves.
 *    In that case we only allow assignments of `false` into that expression
 *    (assignments of `true` will be ignored, and will log a warning)
 * 5. It's a negation of a reversible expression
 *
 * Other Expressions
 * ~~~~~~~~~~~~~~~~~
 * Expressions of other types are reversible (hence not read-only) if and only
 * if ALL the following conditions hold:
 *
 * 1. It's defined simply as the value of a variable, where that variable is a
 *    free variable
 * 2. It's defined simply as the value of a variable, where that variable is
 *    defined with a reversible expression
 */

sealed case class ReadOnlyStatus(nothingToUpdate: Boolean = false, underConstrained: Boolean = false, conditional: Boolean = false, functional: Boolean = false, nonLinear: Boolean = false, otherReversingError: Option[String] = None) {
  def isReadOnly: Boolean = (nothingToUpdate || underConstrained || conditional || functional || nonLinear || otherReversingError != None)
  
  def combineWith (other: ReadOnlyStatus): ReadOnlyStatus = {
    new ReadOnlyStatus(
      this.nothingToUpdate && other.nothingToUpdate,
      this.underConstrained || other.underConstrained,
      this.conditional || other.conditional,
      this.functional || other.functional,
      this.nonLinear || other.nonLinear,
      otherReversingError
    )
  }

  override def toString = {
    var result = List[String]()

    if (nothingToUpdate)
      result ::= "Depends only on read-only/constant expressions"
    
    if (underConstrained)
      result ::= "Depends on two or more free variables"
    
    if (conditional)
      result ::= "Depends on a conditional expression"
    
    if (functional)
      result ::= "Depends on a functional expression"

    if (nonLinear)
      result ::= "Depends on a non-linear expression"

    otherReversingError match {
      case Some(msg) => result ::= msg
      case None =>
    }

    result.mkString(", ")
  }
}

object ReadOnlyStatus {
  val ReadAndWrite = new ReadOnlyStatus()
  val NothingToUpdate = new ReadOnlyStatus(nothingToUpdate = true)
  val UnderConstrained = new ReadOnlyStatus(underConstrained = true)
  val Conditional = new ReadOnlyStatus(conditional = true)
  val Functional = new ReadOnlyStatus(functional = true)
}
